x << y == e:E(Sys). x before y  chain(e) 

latex

---

clarification:

chain-order(es;Sys;chain;x;y) == e:es-E-interface(es;Sys). x before y  chain(e)  Id 

latex

Up	abstract chain replication
Wellformedness Lemmas	chain-order wf
Definitions	x:A. B(x), E(X), x before y  l, f(a), Id
FDL editor aliases	chain-order